Four-Minute Guide to Resolution

Four-Minute Guide to Resolution
Fall 2015, David Matuszek

Resolution is a means of proving statements in the predicate calculus.

A literal is either a proposition, such as P, Q, it_is_raining, or a predicate, such as P(x), R(x,y), female(Sally), mother(Sally, x).
A clause is a disjunction ("or") of zero or more literals, some or all of which may be negated. For example: sinks(x) ∨ dissolves(X, water) ∨ ¬denser(X, water).

Basic principle of resolution:

Given:

A ∨ someLiterals

Conclude:

¬A ∨ someOtherLiterals

someLiterals ∨ someOtherLiterals

Example:

Given:

broke(Bob) ∨ well-fed(Bob)

Conclude:
¬broke(Bob) ∨ ¬hungry(Bob)
well-fed(Bob) ∨ ¬hungry(Bob)

There exists a nine-step algorithm for converting any statement in the predicate calculus into a set of clauses. The most interesting aspects of this algorithm are:
- Existentially quantified (∃) variables become Skolem constants or Skolem functions.
- All remaining variables are assumed to be universally quantified (∀).
Unification is the process of deciding that two literals are "the same". The rules for unification are:
- A variable can be unified with anything.
- Two constants can be unified only if they are identical.
- Two predicates can be unified if and only if their respective arguments can be unified.

Resolution depends on unification. For example:

Given:

broke(x) ∨ well-fed(x)

Conclude:
¬broke(Bob) ∨ ¬hungry(Bob)
well-fed(Bob) ∨ ¬hungry(Bob)where x unifies with Bob

Refutation resolution consists of adding the negation of the clause you want to prove, and trying to get to a contradiction (resolving X with ¬X, yielding NIL, the zero-length clause).
Resolution is complete: anything provable can be proved using only the resolution rule.

Given:	`A ∨ someLiterals`
Conclude:	`¬A ∨ someOtherLiterals` `someLiterals ∨ someOtherLiterals`

Given:	`broke(Bob) ∨ well-fed(Bob)`
Conclude:	`¬broke(Bob) ∨ ¬hungry(Bob)` `well-fed(Bob) ∨ ¬hungry(Bob)`

Given:	`broke(x) ∨ well-fed(x)`
Conclude:	`¬broke(Bob) ∨ ¬hungry(Bob)` `well-fed(Bob) ∨ ¬hungry(Bob)`where `x` unifies with `Bob`